T:Type, eq:EqDecider(T), es:ES, x:Id, e:{e:E| @loc(e)(x:T)} .
(x changed before e)  ((x when e) = (x after (last change to x before e))  T) 

latex

Definitions	Type, x:A  B(x), EqDecider(T), ES, Atom$n, Id, {x:A| B(x)} , if b then t else f fi , b, @e(xv), (x after e), <a, b>, s = t, t  T, x:A. B(x), loc(e), vartype(i;x), P & Q, @i(x:T), P  Q, E, x changed before e, x when e, A c B
Lemmas	assert wf, changed wf, es-E wf, es-dtype wf, event system wf, deq wf, change-to-last-change, es-when wf, es-vartype wf, es-loc wf, subtype rel self, Id wf